We study the foundations of the imperative and functional languages, including semantics and type systems. The special feature of this course is that theory is done in a very practical and hands-on way: we not just prove, but program all the results from first-principles. The basic tool used in the course is Coq proof assistant, which can be regarded as a functional programming language in its own right. It has been used, for example, to verify correctness of Java Card technology, C compilers or, more recently, fragments of x86 architecture.

Lernziele und Kompetenzen:

 

Wissen The students explain the basics of both programming semantics and proof assistants, in particular Coq. Verstehen The students prove theorems using a proof assistant. Anwenden The students transfer proofs into programs and programs into proofs. Analysieren The students examine behaviour of simple programs using formal semantics Evaluieren (Beurteilen) The students evaluate the role played by logic and type theory in scientific approach to programming. Erschaffen The students provide formal semantics to a simple programming language.